SherbyNet - /page/wikibook/entry.mu

Micron Document

`:top

In `F33f`_`[mathematical logic`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Mathematical_logic]`_`f, an `!uninterpreted function`!`:cite-ref-1[`F5bf`_`[1`#cite-note-1]`_`f] or `!function symbol`!`:cite-ref-2[`F5bf`_`[2`#cite-note-2]`_`f] is one that has no other property than its name and `*`F33f`_`[n-ary`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Arity]`_`f`* form. Function symbols are used, together with constants and variables, to form `F33f`_`[terms`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Term_(logic)]`_`f.

The `!theory of uninterpreted functions`! is also sometimes called the `!free theory`!, because it is freely generated, and thus a `F33f`_`[free object`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Free_object]`_`f, or the `!empty theory`!, being the `F33f`_`[theory`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Theory_(mathematical_logic)]`_`f having an empty set of `F33f`_`[sentences`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Sentence_(mathematical_logic)]`_`f (in analogy to an `F33f`_`[initial algebra`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Initial_algebra]`_`f). Theories with a non-empty set of equations are known as `F33f`_`[equational theories`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Equational_theory]`_`f. The `F33f`_`[satisfiability`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Satisfiability]`_`f problem for free theories is solved by `F33f`_`[syntactic unification`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Syntactic_unification]`_`f; algorithms for the latter are used by interpreters for various computer languages, such as `F33f`_`[Prolog`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Prolog]`_`f. Syntactic unification is also used in algorithms for the satisfiability problem for certain other equational theories, see `F33f`_`[Unification (computer science)`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Unification_(computer_science)]`_`f.

>>Contents

• `F0af`_`[Example`#example]`_`f

• `F0af`_`[Discussion`#discussion]`_`f

• `F0af`_`[See also`#see-also]`_`f

• `F0af`_`[Notes`#notes]`_`f

• `F0af`_`[References`#references]`_`f

-─

>>Example

As an example of uninterpreted functions for `F33f`_`[SMT-LIB`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=SMT-LIB]`_`f, if this input is given to an `F33f`_`[SMT solver`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Satisfiability_modulo_theories]`_`f:

`B100`F9d9(declare-fun f (Int) Int)`f`b

`B100`F9d9(assert (= (f 10) 1))`f`b

the SMT solver would return "This input is satisfiable". That happens because `B100`F9d9f`f`b is an uninterpreted function (i.e., all that is known about `B100`F9d9f`f`b is its `F33f`_`[signature`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Signature_(logic)]`_`f), so it is possible that `B100`F9d9f(10) = 1`f`b. But by applying the input below:

`B100`F9d9(declare-fun f (Int) Int)`f`b

`B100`F9d9(assert (= (f 10) 1))`f`b

`B100`F9d9(assert (= (f 10) 42))`f`b

the SMT solver would return "This input is unsatisfiable". That happens because `B100`F9d9f`f`b, being a function, can never return different values for the same input.

>>Discussion

The `F33f`_`[decision problem`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Decision_problem]`_`f for free theories is particularly important, because many theories can be reduced by it.`:cite-ref-3[`F5bf`_`[3`#cite-note-3]`_`f]

Free theories can be solved by searching for `F33f`_`[common subexpressions`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Common_subexpression]`_`f to form the `F33f`_`[congruence closure`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Congruence_closure]`_`f. Solvers include `F33f`_`[satisfiability modulo theories`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Satisfiability_modulo_theories]`_`f solvers.

>>See also

• `F33f`_`[Algebraic data type`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Algebraic_data_type]`_`f

• `F33f`_`[Initial algebra`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Initial_algebra]`_`f

• `F33f`_`[Term algebra`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Term_algebra]`_`f

• `F33f`_`[Theory of pure equality`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Theory_of_pure_equality]`_`f

>>Notes

>>References

`:cite-note-1`!1.`! `F0af`_`[↑`#cite-ref-1]`_`f `:citerefbryantlahiriseshia2002`aBryant, Randal E.; Lahiri, Shuvendu K.; Seshia, Sanjit A. (2002). "Modeling and Verifying Systems Using a Logic of Counter Arithmetic with Lambda Expressions and Uninterpreted Functions" (PDF). `*Computer Aided Verification`*. Lecture Notes in Computer Science. Vol. 2404. pp. 78–92. `F33f`_`[doi`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Doi_(identifier)]`_`f:10.1007/3-540-45657-0_7. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-3-540-43997-4. `F33f`_`[S2CID`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=S2CID_(identifier)]`_`f 9471360.

`:cite-note-2`!2.`! `F0af`_`[↑`#cite-ref-2]`_`f `:citerefbaadernipkow1999`a`F33f`_`[Baader, Franz`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Franz_Baader]`_`f; `F33f`_`[Nipkow, Tobias`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=Tobias_Nipkow]`_`f (1999). `*Term Rewriting and All That`*. Cambridge University Press. p. 34. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-0-521-77920-3.

`:cite-note-3`!3.`! `F0af`_`[↑`#cite-ref-3]`_`f `:citerefde-mourabj-rner2009`ade Moura, Leonardo; Bjørner, Nikolaj (2009). `*Formal methods : foundations and applications : 12th Brazilian Symposium on Formal Methods, SBMF 2009, Gramado, Brazil, August 19-21, 2009 : revised selected papers`* (PDF). Berlin: Springer. `F33f`_`[ISBN`:/page/wikibook/entry.mu`zim=wikipedia_en_all_nopic_2025-08.zim|entry_path=ISBN_(identifier)]`_`f 978-3-642-10452-7.

`c`F0af`_`[↑ Back to top`#top]`_`f`a